import Yices
import Data.List hiding (sort)
{-
import Test.QuickCheck hiding (Prop)
import qualified Test.QuickCheck as Q
-}

-- A row is the state of the array at a concrete timepoint
type Row = Nat -> Term Nat

-- Some constants for better flexibility
slots = 12  -- how many items in the array
steps = 5   -- how many iterations to perform

-- Declare used variables
s' :: Ident (Nat -> Nat -> Nat)
(s',s) = ident2 "s"

m' :: Ident (Nat -> Nat -> Nat)
(m',m) = ident2 "m"

n' :: Ident (Nat -> Nat -> Nat)
(n',n) = ident2 "n"

-- Initial condition
initial :: Row -> Prop
initial f =
    conj [f i <= (slots-1) | i <- [0..slots-1]]                   -- every element <= slots-1
    /\ conj [f i /= f j | i <- [0..slots-2], j <- [i+1..slots-1]]  -- all elements different
  where
    x <= y = idt le' ! x ! nat y
    x /= y = non (idt eq' ! x ! y)

-- Final condition
final :: Row -> Prop
final f =
    disj [f i > f (i+1) | i <- [0..slots-2]] -- there are some unsorted neighbors
  where
    x > y = idt gt' ! x ! y

-- Transition (at step i, turn x into y)
trans :: Nat -> Row -> Row -> Prop
trans i x y = 
    -- halfsort turns x --> m i
    conj [sort j (slots-1-j) x (m i) | j <- [0..(slots `div` 2)-1]]
    -- pairsort turns m i --> y (using n i as an intermediate array)
    /\ pairsort (m i) (n i) y
  where
    sort :: Nat -> Nat -> Row -> Row -> Prop
    sort i j x y = ifte (x i < x j) ((x i == y i) /\ (x j == y j)) ((x i == y j) /\ (x j == y i))
    x < y = idt lt' ! x ! y
    (==) :: Term Nat -> Term Nat -> Prop
    x == y = idt eq' ! x ! y

-- Smart pairsort, calculating O(N) pairswaps in two steps
pairsort :: Row -> Row -> Row -> Prop
pairsort m n y =
    (n 0) == (m 0)
    /\ conj [ifte (m i > n (i-1)) (n i == m i) (n i == n (i-1)) | i <- [1..slots-1]]
    /\ conj [ifte (n i < m (i+1)) (y i == n i) (y i == m (i+1)) | i <- [0..slots-2]]
    /\ y (slots-1) == n (slots-1)
  where
    x < y = idt lt' ! x ! y
    x > y = idt gt' ! x ! y
    x == y = idt eq' ! x ! y

-- Main program
script =
    -- Define the used types and variables
    [ define s', define m', define n'
    , assert $ initial (s $ 0)
    , assert $ final   (s $ steps)
    , assert $ conj [trans i (s i) (s $ i+1) | i <- [0..steps-1]]
    ]

{-
-- Some QuickCheck properties to test the lemma
bubble :: [Int] -> [Int]
bubble (x:y:xs)
    | x < y     = x : bubble (y:xs)
    | otherwise = y : bubble (x:xs)
bubble xs = xs

-- The lemma in question
lemma :: [Int] -> Bool
lemma [] = True
lemma xs = ys == [min x y | (x,y) <- zip x' y']
  where
    ys = bubble xs
    y' = map maximum (tail $ inits xs)
    x' = tail xs ++ [maximum xs]
-}

main = printScript script
